TerminationOnIrrelevantArgument.agda:35,16-21
Cannot pattern match against irrelevant argument of type Ty empty
when checking that the pattern Empty has type Ty empty
